\subsubsection{表决选择}\label{sec:timers}

如果所有的节点都设置$b$为相同的表决，那么在\todo{页xxx}的第1-6步\todo{xxx}足够认可表决的值并且具体化它。然而，在表决协议开始时提名协议并不一定已经在每处都产生了相同的值，在这种情形下节点可能会在它们尝试提交第一个表决的时候失败。如果一个表决失败了或花费了太多的时间那么它可能因为没有响应的节点而失败，那么该节点必须增加它的表决计数器而重新用一个更高的表决来尝试。

当转用新的表决时，节点$v$设置$b_v\leftarrow \langle b_v.n+1,z\rangle$，这里$z$是由这个决定的：如果$P\neq \mybm{0}$，那么$z=P.x$；否则，$z$是合成值$combine(Z)$，这里$Z$是第\ref{sec:scp_nominate_concrete}节提到的候选值。由于$c$总是由$P=b$初始化而来，提高$P.x$的优先级确保在每个节点处有不变量：如果$c\neq \mybm{0}$那么$c\lesssim P\lesssim b$。

方便起见，我们用下标来区分属于特别的节点或消息的域。如果$v$是一个节点，那么用$b_v$，$p_v$，$p_v^{\prime}\ldots$表示{图\ref{fig:state}}中描述的节点$v$的状态值$b,p,p^{\prime}\ldots$。我们还设置$z_v$为上文提到的$v$的下一个表决——即，如果$P\neq \mybm{0}$那么$z_v$为$P_v.x$否则是$v$的合成值。类似地，令$b_m,p_m,p^{\prime}_m,P_m,c_m$表示在{图\ref{fig:messages}}中所描述的由一个网络消息$m$包含的对应的域。

\begin{definition}[自我验证]
	称在节点$v$处的消息集合$S\subseteq M_v$是\textit{自我验证}的，当$v$是$S$中的某个发送者而$S$的发送者集合是一个在消息的$D$域下、声明的{\quorum}集合之下的一个{\quorum}。
\end{definition}

一个节点应当在$\varphi=\textsl{PREPARE}$且下面条件之一满足的情况下放弃当前的表决$b_v$而转向一个更高的表决：

\begin{enumerate}
	\item\label{enum:giveup1} $M_v$包含一个来自发送者的{\vblock}集合的消息集合$S$，使得$\forall m\in S,b_v.n<b_m.n$且要么$b_m.n=\infty$要么$P_v\lesssim c_m$ (意味着$v$的表决计数器已经落后了)。
	\item\label{enum:giveup2} 自从$M_v$第一次包含一个自我验证的集合$S$(满足$\forall m\in S,b_v.n<b_m.n$)之后已经超时过期了(意味着$b_v$可能将不会提交陈述，且$v$希望它已经收到了足够多的消息来选择一个更好的新表决)。
\end{enumerate}

为了确保协议最终能够结束，条件\ref{enum:giveup2}必须足够长以使得所有良性行为节点能够交换数轮消息。为了在不需要预测网络延迟的情形下达成这个具体的实现，超时值应当设置为随着$b_v.n$的增长而增长。同样需要注意，当节点$v$已经落后时，并不是遍历测试每个计数器，而是可以简单地增加$b_v.n$到使得条件\ref{enum:giveup1}为假的最小值。